Nuprl Lemma : no-member-sq-nil
11,40
postcript
pdf
T
:Type,
L
:(
T
List). (
x
:
T
.
(
x
L
))
(
L
~ [])
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
,
P
Q
,
SQType(
T
)
,
A
,
P
Q
,
P
Q
,
P
&
Q
,
False
,
{
T
}
Lemmas
not
wf
,
l
member
wf
,
cons
member
origin
T:Type, L:(T List). (x:T. 
(x 
L)) 
(L ~ []) T:Type, L:(T List). (x:T. (x L)) (L ~ []) x:A. B(x) Q T
QA
Q Q